Nuprl Definition : monotone
13,42
postcript
pdf
monotone(
T
;
T'
;
x
,
y
.
R
(
x
;
y
);
x
,
y
.
R'
(
x
;
y
);
f
) ==
x
,
y
:
T
.
R
(
x
;
y
)
R'
(
f
(
x
);
f
(
y
))
latex
clarification:
monotone(
T
;
T'
;
x
,
y
.
R
(
x
;
y
);
x
,
y
.
R'
(
x
;
y
);
f
) ==
x
:
T
,
y
:
T
.
R
(
x
;
y
)
R'
(
f
(
x
);
f
(
y
))
latex
Up
gen
algebra
1
Wellformedness Lemmas
monotone
wf
Definitions
x
:
A
.
B
(
x
)
,
P
Q
origin
x, y:T. R(x;y) 
R'(f(x);f(y))
x:T, y:T. R(x;y) R'(f(x);f(y)) x, y:T. R(x;y) R'(f(x);f(y))
x:T, y:T. R(x;y) R'(f(x);f(y)) x:A. B(x) Q